home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
kermit.columbia.edu
/
kermit.columbia.edu.tar
/
kermit.columbia.edu
/
newsgroups
/
misc.19950528-19950726
/
000405_news@columbia.edu_Fri Jul 21 20:10:18 1995.msg
< prev
next >
Wrap
Internet Message Format
|
1995-07-31
|
3KB
Received: from apakabar.cc.columbia.edu by watsun.cc.columbia.edu with SMTP id AA18084
(5.65c+CU/IDA-1.4.4/HLK for <kermit.misc@watsun.cc.columbia.edu>); Fri, 21 Jul 1995 16:59:43 -0400
Received: by apakabar.cc.columbia.edu id AA19054
(5.65c+CU/IDA-1.4.4/HLK for kermit.misc@watsun); Fri, 21 Jul 1995 16:59:41 -0400
Path: news.columbia.edu!panix!news.mathworks.com!newshost.marcam.com!zip.eecs.umich.edu!news-server.eecs.umich.edu!huggins
From: huggins@tarski.eecs.umich.edu (James K. Huggins)
Newsgroups: comp.protocols.kermit.misc
Subject: Kermit Proof of Correctness Available
Followup-To: comp.protocols.kermit.misc
Date: 21 Jul 1995 20:10:18 GMT
Organization: University of Michigan EECS Dept., Ann Arbor, MI
Lines: 38
Distribution: world
Message-Id: <HUGGINS.95Jul21161018@tarski.eecs.umich.edu>
Nntp-Posting-Host: tarski.eecs.umich.edu
Apparently-To: kermit.misc@watsun.cc.columbia.edu
In his preface to Frank da Cruz's book Kermit: A File Transfer
Protocol, Don Knuth wrote:
I hope that many readers of this book will be challenged to find
high-level concepts and invariant relations by which various
versions of the Kermit protocol can be proved correct in a
mathematical sense.
I'm pleased to announce that such a proof has recently been completed.
The proof gives a complete specification of the core Kermit file
transfer protocol, and shows that it is both safe (if you get a file,
you can be sure it's the one that was sent) and live (if you send
a file, and the network isn't too bad, it gets to the other end).
The proof (written by myself) appears as part of a new book,
"Specification and Validation Methods", edited by Egon Boerger
and available through Oxford University Press (ISBN 0-19-853854-5,
official publishing date 3 August 1995).
Thanks to the good folks at Oxford University Press, as well as Frank
da Cruz at Columbia, the Kermit proof has been made available
as part of the Kermit repository at Columbia University. Those of
you with WWW access can find the cover page for the proof, including
more detailed information on the book containing the proof, at
http://www.columbia.edu/kermit/proof.html
The proof itself (in PostScript) is available via anonymous FTP as
ftp://kermit.columbia.edu/kermit/e/proof.ps
As the author of the proof, I'd be happy to hear any comments or
questions you might have about the proof. The proof uses a relatively
new specification methodology known as "evolving algebras"; an
introduction to the method is contained in the proof. I'd be happy
to discuss the technique with anyone who might be interested.
Jim Huggins (huggins@umich.edu)